(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun x1 () U)
(declare-fun x2 () U)
(declare-fun x3 () U)
(declare-fun x4 () U)
(declare-fun x5 () U)
(declare-fun x6 () U)
(declare-fun x7 () U)
(declare-fun x8 () U)

(assert (and
 (distinct x0 x1 x2)
 (distinct x0 x1 x3)
 (distinct x0 x1 x4)
 (distinct x0 x1 x5)
 (distinct x0 x1 x6)
 (distinct x0 x1 x7)
 (distinct x0 x1 x8)
 (distinct x0 x2 x3)
 (distinct x0 x2 x4)
 (distinct x0 x2 x5)
 (distinct x0 x2 x6)
 (distinct x0 x2 x7)
 (distinct x0 x2 x8)
 (distinct x0 x3 x4)
 (distinct x0 x3 x5)
 (distinct x0 x3 x6)
 (distinct x0 x3 x7)
 (distinct x0 x3 x8)
 (distinct x0 x4 x5)
 (distinct x0 x4 x6)
 (distinct x0 x4 x7)
 (distinct x0 x4 x8)
 (distinct x0 x5 x6)
 (distinct x0 x5 x7)
 (distinct x0 x5 x8)
 (distinct x0 x6 x7)
 (distinct x0 x6 x8)
 (distinct x0 x7 x8)
 (distinct x1 x2 x3)
 (distinct x1 x2 x4)
 (distinct x1 x2 x5)
 (distinct x1 x2 x6)
 (distinct x1 x2 x7)
 (distinct x1 x2 x8)
 (distinct x1 x3 x4)
 (distinct x1 x3 x5)
 (distinct x1 x3 x6)
 (distinct x1 x3 x7)
 (distinct x1 x3 x8)
 (distinct x1 x4 x5)
 (distinct x1 x4 x6)
 (distinct x1 x4 x7)
 (distinct x1 x4 x8)
 (distinct x1 x5 x6)
 (distinct x1 x5 x7)
 (distinct x1 x5 x8)
 (distinct x1 x6 x7)
 (distinct x1 x6 x8)
 (distinct x1 x7 x8)
 (distinct x2 x3 x4)
 (distinct x2 x3 x5)
 (distinct x2 x3 x6)
 (distinct x2 x3 x7)
 (distinct x2 x3 x8)
 (distinct x2 x4 x5)
 (distinct x2 x4 x6)
 (distinct x2 x4 x7)
 (distinct x2 x4 x8)
 (distinct x2 x5 x6)
 (distinct x2 x5 x7)
 (distinct x2 x5 x8)
 (distinct x2 x6 x7)
 (distinct x2 x6 x8)
 (distinct x2 x7 x8)
 (distinct x3 x4 x5)
 (distinct x3 x4 x6)
 (distinct x3 x4 x7)
 (distinct x3 x4 x8)
 (distinct x3 x5 x6)
 (distinct x3 x5 x7)
 (distinct x3 x5 x8)
 (distinct x3 x6 x7)
 (distinct x3 x6 x8)
 (distinct x3 x7 x8)
 (distinct x4 x5 x6)
 (distinct x4 x5 x7)
 (distinct x4 x5 x8)
 (distinct x4 x6 x7)
 (distinct x4 x6 x8)
 (distinct x4 x7 x8)
 (distinct x5 x6 x7)
 (distinct x5 x6 x8)
 (distinct x5 x7 x8)
 (distinct x6 x7 x8)))
(check-sat)
(exit)
